\begin{tabbing}
only $k$($v$):$B$ sends [${\it tg}$,$f$($s$;$v$)] : $T$ on $l$
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(\=$\forall$$e$:E.\+\+
\\[0ex](loc($e$) = source($l$))
\\[0ex]$\Rightarrow$ (kind($e$) = $k$)
\\[0ex]$\Rightarrow$ ($\exists$${\it e'}$:E. ((kind(${\it e'}$) = rcv($l$,${\it tg}$)) c$\wedge$ (sender(${\it e'}$) = $e$))))
\-\\[0ex]\& (\=$\forall$${\it e'}$:E.\+
\\[0ex](kind(${\it e'}$) = rcv($l$,${\it tg}$))
\\[0ex]$\Rightarrow$ \=((kind(sender(${\it e'}$)) = $k$)\+
\\[0ex]c$\wedge$ (valtype(sender(${\it e'}$)) $\subseteq$r $B$)
\\[0ex]c$\wedge$ (valtype(${\it e'}$) $\subseteq$r $T$)
\\[0ex]c$\wedge$ \=(val(${\it e'}$) = $f$((state when sender(${\it e'}$));val(sender(${\it e'}$)))\+
\\[0ex]\& (\=$\forall$${\it e''}$:E.\+
\\[0ex](kind(${\it e''}$) = rcv($l$,${\it tg}$)) $\Rightarrow$ (sender(${\it e''}$) = sender(${\it e'}$)) $\Rightarrow$ (${\it e''}$ = ${\it e'}$)))))
\-\-\-\-\-
\end{tabbing}